Jean-Yves
Nous quittons alors les vérités pérennes pour vivre dans l'instant : en termes linguistiques, nous passons de l'imparfait au parfait. L'infini retrouve ainsi son étymologie (imparfaite) : celle du non-terminé. Epistémologiquement, le texte rompt avec la sempiternelle polarisation entre réalisme et anti-réalisme, en lui substituant l'opposition entre existence et essence. D'ontologique, la question devient morphologique : la logique est-elle antérieure aux phénomènes qu'elle contrôle ? Cet ouvrage est le premier d'une publication en deux volumes ce n'est qu'au second tome, avec l'analyse de l'imperfection, que nous arriverons à la pérennité non pérenne ; c'est un peu la réconciliation de l'essence et de l'existence sur d'autres bases que la familière combinatoire logistique : les algèbres d'opérateurs.
Le premier tome Vers la perfection s'achevait sur la logique linéaire et la distinction entre parfait et imparfait : le parfait renvoie à un monde d'actions où l'on vit dans l'instant loin des vérités pérennes, alors que l'imparfait est le monde de l'infini et de la pérennité, lieu du non-terminé. Alors que la perfection s'analyse sans problème, tous les paradigmes logiques considérés deviennent problématiques hors du mode parfait.
Dans ce second tome, Vers l'imperfection, nous interrogeons ce monde imparfait. En particulier, comment postuler la pérennité sans postuler en même temps la pérennité de la pérennité ? Une pérennité non pérenne s'exprime cependant dans les logiques iconoclastes, des systèmes qui font sens sur le papier, mais qu'on a du mal à asseoir : la bonne intuition se trouve finalement du côté de la mécanique quantique et des algèbres d'opérateurs : c'est la géométrie de l'interaction. L'interprétation de l'imperfection suppose la reconnaissance de l'intrication entre sujet et objet : on découvre in fine que la tradition logique a minimisé le rôle du sujet ; paradoxalement, en cherchant des notions objectives, elle est tombée dans le subjectivisme. Le premier tome s'ouvrait sur l'essentialisme arrogant de Tarski : la vérité est la dualité de ce qui est vrai.
Le second tome lui répond en se refermant sur une définition subjective de la vérité, qui tient (enfin) compte de la place prépondérante du sujet dans l'énonciation.
GIRARD Jean-Yves
Statut Directeur de recherches CNRS à Marseille, où je dirige l'équipe de Logique de la Programmation au sein de l'Institut de Mathématiques de Luminy (ci-devant Laboratoire de Mathématiques Discrètes) UPR 9016. Diplômes Docteur et agrégé de mathématiques.
Parcours
- 1992--- : Directeur de recherches CNRS à Marseille, y dirige l'équipe de Logique de la Programmation au sein de l'Institut de Mathématiques de Luminy (ci-devant Laboratoire de Mathématiques Discrètes) UPR 9016.
- 1991-1995 : Membre élu du Comité National (section 01).
- 1990-1992 : Directeur de recherches CNRS, à l'Université Paris VII, dans l'Equipe de Logique Mathématique (UA 753).
- 1989-1991 : conseiller scientifique auprès du projet FORMEL de l'INRIA, dirigé par Gérard Huet.
- 1983-1986 : Membre nommé du Comité National (section 03).
- 1981--- : Maître de recherches (DR2) au CNRS.
- 1973-1981 : Chargé de recherches au CNRS.
- 1971--- : Entre au CNRS.
- 1971-1992 : Professeur à Paris VII.
- 1966-1970 : Elève-Maître à l'ENS de St Cloud, Lyon, Montepellier.
- 1962-1965 : élève-maître à l'Ecole Normale d'Instituteurs de Lyon. Prix
- 1990 : Prix Poncelet de l'Académie des Sciences.
- 1983 : Médaille d'Argent du CNRS. Spécialités logique, informatique théorique, mathématiques https://drive.google.com/open?id=1q9d... https://www.canal-u.tv/video/universi...
GENTZEN
Gerhard,
source W,
de Gerthard GENTZEN à Jean-Yves GIRARD,
par Baptiste MELES, HAL, .pdf, 2015,
déduction,
logique du 1er ordre, (et aussi),
déduction naturelle,
séquent, calcul des séquents,
par J-B.JOINET, HAL, .pdf, 2014,
Recherches sur la déduction logique,
GENTZEN.Gerhard, 1955, PUF,
Etude sur l'inférence logique, en allemand, SUB, 176 à 180, lire en ligne, 1934, GENTZEN;
Collected Papers of Gerhard Gentzen, M. E. Szabo (éd.), Amsterdam, Hollande-Septentrionale, 1969.
principe d'induction,
ordinal,
Théorie de la démonstration,
théorème d'incimplétude de Gödel,
programme de HILBERT,
Gentzen a d'autre part démontré la cohérence de l'arithmétique de Peano (en 1936) en utilisant un principe d'induction jusqu'à l'ordinal dénombrable ε0, mais pour des formules de faible complexité logique. Les méthodes utilisées pour cette démonstration se sont révélées essentielles pour la théorie de la démonstration moderne.
La théorie dans laquelle cette démonstration peut se formaliser est nécessairement plus forte que l'arithmétique de Peano d'après le second théorème d'incomplétude de Gödel (au sens où si elle permet de démontrer la cohérence de l'arithmétique de Peano, sa cohérence ne pourra donc se démontrer dans cette arithmétique). On a pu voir cette démonstration, à laquelle Gödel s'est beaucoup intéressé, comme une tentative pour réhabiliter le programme de Hilbert, en élargissant la notion de méthodes finitaires à des récurrences jusqu'à certains ordinaux comme ε0. La cohérence de la théorie utilisée par Gentzen pour sa démonstration, bien que plus forte, serait moins douteuse que la cohérence de l'arithmétique de Peano, parce que l'induction, bien que jusqu'à un ordinal (forcément supérieur à celui des entiers), se fait sur des formules simples. Cette dernière affirmation n'a plus guère de défenseurs. De façon plus objective, cette démonstration permet d'analyser les raisons de la cohérence de l'arithmétique de Peano ; par exemple le résultat de cohérence permet d'en mesurer la « force » comme le traduit l'utilisation de l'ordinal ε0. En généralisant ce principe, on a pu engager une classification des théories arithmétiques.
Esquisse d'une grammaire pure, Jean-Louis GARDIES, Vrin,
book-google,
GENTZEN, La cohérence des nombres purs, Ann., 112 (1936), 493-565. Traduction française La consistance de l'arithmétique élémentaire par Jean Largeault, in Intuitionisme et théorie de la démonstration pages 285-357 Paris, Vrin, 1992
Nouvelle version de la preuve de cohérence pour la théorie pure des nombres, recherches sur la logique et le fondement des sciences exactes, nouvelle série, tome 4, p. 19-44. S. Hirzel, Leipzig, 1938.
Traduction française Nouvelle version de la démonstration de consistance pour l'arithmétique élémentaire par Jean Largeault, in Intuitionisme et théorie de la démonstration pages 359-394 Paris, Vrin, 1992